KILLEDRuntime Complexity (full) proof of /tmp/tmptN4gky/Ex4_7_37_Bor03.xml
The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).0 CpxTRS↳1 RenamingProof (⇔, 0 ms)↳2 CpxRelTRS↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)↳4 typed CpxTrs↳5 OrderProof (LOWER BOUND(ID), 0 ms)↳6 typed CpxTrs↳7 NoRewriteLemmaProof (LOWER BOUND(ID), 354 ms)↳8 typed CpxTrs↳9 RewriteLemmaProof (LOWER BOUND(ID), 193 ms)↳10 BEST↳11 typed CpxTrs↳12 RewriteLemmaProof (LOWER BOUND(ID), 5 ms)↳13 BEST↳14 typed CpxTrs↳15 NoRewriteLemmaProof (LOWER BOUND(ID), 13 ms)↳16 typed CpxTrs↳17 typed CpxTrs↳18 typed CpxTrs(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
from(X) → cons(X, from(s(X)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0) → 0
minus(s(X), s(Y)) → minus(X, Y)
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Rewrite Strategy: FULL(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
S is empty.
Rewrite Strategy: FULL(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.(4) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'(5) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
from, sel, minus, quot, zWquotThey will be analysed ascendingly in the following order:
minus < quot
quot < zWquot(6) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'Generator Equations:
gen_cons:nil3_0(0) ⇔ nil
gen_cons:nil3_0(+(x, 1)) ⇔ cons(0', gen_cons:nil3_0(x))
gen_s:0'4_0(0) ⇔ 0'
gen_s:0'4_0(+(x, 1)) ⇔ s(gen_s:0'4_0(x))The following defined symbols remain to be analysed:
from, sel, minus, quot, zWquotThey will be analysed ascendingly in the following order:
minus < quot
quot < zWquot(7) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol from.(8) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'Generator Equations:
gen_cons:nil3_0(0) ⇔ nil
gen_cons:nil3_0(+(x, 1)) ⇔ cons(0', gen_cons:nil3_0(x))
gen_s:0'4_0(0) ⇔ 0'
gen_s:0'4_0(+(x, 1)) ⇔ s(gen_s:0'4_0(x))The following defined symbols remain to be analysed:
sel, minus, quot, zWquotThey will be analysed ascendingly in the following order:
minus < quot
quot < zWquot(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
sel(gen_s:0'4_0(n57_0), gen_cons:nil3_0(+(1, n57_0))) → gen_s:0'4_0(0), rt ∈ Ω(1 + n570)Induction Base:
sel(gen_s:0'4_0(0), gen_cons:nil3_0(+(1, 0))) →RΩ(1)
0'Induction Step:
sel(gen_s:0'4_0(+(n57_0, 1)), gen_cons:nil3_0(+(1, +(n57_0, 1)))) →RΩ(1)
sel(gen_s:0'4_0(n57_0), gen_cons:nil3_0(+(1, n57_0))) →IH
gen_s:0'4_0(0)We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'Lemmas:
sel(gen_s:0'4_0(n57_0), gen_cons:nil3_0(+(1, n57_0))) → gen_s:0'4_0(0), rt ∈ Ω(1 + n570)Generator Equations:
gen_cons:nil3_0(0) ⇔ nil
gen_cons:nil3_0(+(x, 1)) ⇔ cons(0', gen_cons:nil3_0(x))
gen_s:0'4_0(0) ⇔ 0'
gen_s:0'4_0(+(x, 1)) ⇔ s(gen_s:0'4_0(x))The following defined symbols remain to be analysed:
minus, quot, zWquotThey will be analysed ascendingly in the following order:
minus < quot
quot < zWquot(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
minus(gen_s:0'4_0(n364_0), gen_s:0'4_0(n364_0)) → gen_s:0'4_0(0), rt ∈ Ω(1 + n3640)Induction Base:
minus(gen_s:0'4_0(0), gen_s:0'4_0(0)) →RΩ(1)
0'Induction Step:
minus(gen_s:0'4_0(+(n364_0, 1)), gen_s:0'4_0(+(n364_0, 1))) →RΩ(1)
minus(gen_s:0'4_0(n364_0), gen_s:0'4_0(n364_0)) →IH
gen_s:0'4_0(0)We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(13) Complex Obligation (BEST)
(14) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'Lemmas:
sel(gen_s:0'4_0(n57_0), gen_cons:nil3_0(+(1, n57_0))) → gen_s:0'4_0(0), rt ∈ Ω(1 + n570)
minus(gen_s:0'4_0(n364_0), gen_s:0'4_0(n364_0)) → gen_s:0'4_0(0), rt ∈ Ω(1 + n3640)Generator Equations:
gen_cons:nil3_0(0) ⇔ nil
gen_cons:nil3_0(+(x, 1)) ⇔ cons(0', gen_cons:nil3_0(x))
gen_s:0'4_0(0) ⇔ 0'
gen_s:0'4_0(+(x, 1)) ⇔ s(gen_s:0'4_0(x))The following defined symbols remain to be analysed:
quot, zWquotThey will be analysed ascendingly in the following order:
quot < zWquot(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol quot.(16) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'Lemmas:
sel(gen_s:0'4_0(n57_0), gen_cons:nil3_0(+(1, n57_0))) → gen_s:0'4_0(0), rt ∈ Ω(1 + n570)
minus(gen_s:0'4_0(n364_0), gen_s:0'4_0(n364_0)) → gen_s:0'4_0(0), rt ∈ Ω(1 + n3640)Generator Equations:
gen_cons:nil3_0(0) ⇔ nil
gen_cons:nil3_0(+(x, 1)) ⇔ cons(0', gen_cons:nil3_0(x))
gen_s:0'4_0(0) ⇔ 0'
gen_s:0'4_0(+(x, 1)) ⇔ s(gen_s:0'4_0(x))The following defined symbols remain to be analysed:
zWquot(17) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'Lemmas:
sel(gen_s:0'4_0(n57_0), gen_cons:nil3_0(+(1, n57_0))) → gen_s:0'4_0(0), rt ∈ Ω(1 + n570)
minus(gen_s:0'4_0(n364_0), gen_s:0'4_0(n364_0)) → gen_s:0'4_0(0), rt ∈ Ω(1 + n3640)Generator Equations:
gen_cons:nil3_0(0) ⇔ nil
gen_cons:nil3_0(+(x, 1)) ⇔ cons(0', gen_cons:nil3_0(x))
gen_s:0'4_0(0) ⇔ 0'
gen_s:0'4_0(+(x, 1)) ⇔ s(gen_s:0'4_0(x))No more defined symbols left to analyse.
(18) Obligation:
TRS:
Rules:
from(X) → cons(X, from(s(X)))
sel(0', cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
minus(X, 0') → 0'
minus(s(X), s(Y)) → minus(X, Y)
quot(0', s(Y)) → 0'
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) → nil
zWquot(nil, XS) → nil
zWquot(cons(X, XS), cons(Y, YS)) → cons(quot(X, Y), zWquot(XS, YS))
Types:
from :: s:0' → cons:nil
cons :: s:0' → cons:nil → cons:nil
s :: s:0' → s:0'
sel :: s:0' → cons:nil → s:0'
0' :: s:0'
minus :: s:0' → s:0' → s:0'
quot :: s:0' → s:0' → s:0'
zWquot :: cons:nil → cons:nil → cons:nil
nil :: cons:nil
hole_cons:nil1_0 :: cons:nil
hole_s:0'2_0 :: s:0'
gen_cons:nil3_0 :: Nat → cons:nil
gen_s:0'4_0 :: Nat → s:0'Lemmas:
sel(gen_s:0'4_0(n57_0), gen_cons:nil3_0(+(1, n57_0))) → gen_s:0'4_0(0), rt ∈ Ω(1 + n570)Generator Equations:
gen_cons:nil3_0(0) ⇔ nil
gen_cons:nil3_0(+(x, 1)) ⇔ cons(0', gen_cons:nil3_0(x))
gen_s:0'4_0(0) ⇔ 0'
gen_s:0'4_0(+(x, 1)) ⇔ s(gen_s:0'4_0(x))No more defined symbols left to analyse.